Hardware verification is currently the bottleneck and the most expensive task in the design of a semiconductor integrated circuit. Model checking is a method of formal verification that is gaining in popularity for this purpose. The method is described generally by Clarke et 1. in Model Checking (MIT Press, 1999).
To perform model checking of the design of a device, a verification engineer reads the definition and functional specifications of the device and then, based on this information, writes a set of properties {φ} (also known as a specification) that the design is expected to fulfill. The properties are written in a suitable specification language for expressing temporal logic relationships between the inputs and outputs of the device. Such languages are commonly based on Computation Tree Logic (CTL). A hardware model M (also known as an implementation) of the design, which is typically written in a hardware description language, such as VHDL or Verilog, is then tested to ascertain that the model satisfies all of the properties in the set, i.e., that Mφ, under all possible input sequences. Such testing is a form of reachability analysis.
Model checking is preferably carried out automatically by a symbolic model checking program, such as SMV, as described, for example, by McMillan in Symbolic Model Checking (Kluwer Academic Publishers, 1993). A number of practical model checking tools are available, among them RuleBase, developed by IBM, which is described by Beer et al. in “RuleBase: an Industry-Oriented Form Verification Tool,” in Proceedings of the Design Automation Conference DAC'96 (Las Vegas, Nev., 1996).
As hardware devices grow larger and more complex, the set of properties needed for model checking becomes unwieldy. The verification engineer has no systematic way to be sure of whether the property set is complete, in the sense of covering all possible states and transitions that may occur in the model. If the property set is incomplete, a bug in the design may go undetected. The engineer may therefore continue to add more and more properties indefinitely, never knowing whether the set is yet sufficient or not.
Coverage metrics have been applied in various fields of simulation-based verification in order to measure and improve the completeness with which a given simulation tool represents the actual behavior of a target system. An application of such a metric to model checking is described by Hoskote et al., in “Coverage Estimation for Symbolic Model Checking,” in Proceedings of the Design Automation Conference DAC'99 (IEEE Computer Society Press, 199). This publication presents a method for estimating whether a set of properties is sufficient to cover all possible states of a model. It notes, however, that the disclosed method cannot point out functionality that may be missing in the model, nor can it ensure that all possible paths between the states are covered. The publication also indicates that “path coverage would be an ideal coverage metric because it can provide coverage of actual executions of the circuit over time.” The publication considers that by comparison with state coverage, “path coverage is a much more intractable problem.”